2020-05-10 11:54:11 (GMT)
Another problem that shows how imporant it is to reason with formulas just like with ordinary terms.
The key step in the proof is to perform superposition between
in X4 (#sk37 F1 X2) = ·∃ λ (Y0:ι). ((in Y0 X2 ∧ F1 Y0 X4)) and in (#sk22 X1) X1
≠ ·∃ λ (Y0:ι). ((in Y0 #sk1 ∧ #sk22 X1= #sk8 Y0)
This gives rise to a literal ·∃ λ (Y0:ι). ((in Y0 X1 ∧ F0 Y0 (#sk22 (#sk37 F0 X1)))) ≠ ·∃ λ (Y0:ι). ((in Y0 #sk1 ∧ #sk22 (#sk37 F0 X1)= #sk8 Y0)) which is resolved by a relatively complicated unifier,
and from that point on proof is simple
2020-05-10 11:55:43 (GMT)
@Alexander Bentkamp @Visa @Sophie This example shows that we should take reasoning with equalities very seriously (like Stuber and Ganzinger)
2020-05-10 21:39:50 (GMT)
This is getting into pretty advanced HO steps…
2020-05-11 7:25:34 (GMT)
I think our calculus will be able to do this. Asymmetric Cases might work better than symmetric Cases for this example.